/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BDR30/FONT#2=BAXM30/FONT#3=BASB30/FONT#4=BDR30/FONT#5=SUB/FONT#6=SUP/FONT#9=FIX40/FONT#10=FIX30/FONT#11=GRFX25/FONT#12=GRFX35
␈↓ ↓N␈↓α␈↓ ←1


␈↓ ↓N␈↓α␈↓ ∧*1.  PROVING LISP PROGRAMS CORRECT


␈↓ ↓N␈↓In␈α∞this␈α∞chapter␈α∞we␈α∞will␈α∞introduce␈α∂techniques␈α∞for␈α∞proving␈α∞LISP␈α∞programs␈α∞correct.␈α∂ The␈α∞techniques
␈↓ ↓N␈↓will␈α
mainly␈α
be␈α∞limited␈α
to␈α
what␈α∞we␈α
may␈α
call␈α
␈↓αclean␈↓␈α∞LISP␈α
programs.␈α
 In␈α∞particular,␈α
there␈α
must␈α∞be␈α
no
␈↓ ↓N␈↓side␈α∃effects,␈α∃because␈α∃our␈α∃methods␈α∃depend␈α∃on␈α∃the␈α∃ability␈α∃to␈α∃replace␈α∃subexpressions␈α⊗by␈α∃equal
␈↓ ↓N␈↓expressions.



␈↓ ↓N␈↓α␈↓ ∧␈1.1 Proofs by structural induction.

␈↓ ↓N␈↓Recall that the operation of appending two lists is defined by

␈↓ ↓N␈↓␈↓α1.1)␈↓ α> x * y ← ␈↓βif n␈↓α x ␈↓βthen␈↓α y ␈↓βelse a␈↓α x . [␈↓βd␈↓α x * y]␈↓.

␈↓ ↓N␈↓Because␈α␈↓αx*y␈↓␈αis␈αdefined␈αfor␈αall␈α␈↓αx␈↓␈αand␈α␈↓αy␈↓,␈αi.e.␈αthe␈αcomputation␈αdescribed␈αabove␈αterminates␈αfor␈αall␈α␈↓αx␈↓␈αand
␈↓ ↓N␈↓␈↓αy␈↓, we can replace (1.1) by the sentence

␈↓ ↓N␈↓␈↓α1.2)␈↓ α> ∀x y:[islist x ∧ islist y ⊃ [x * y = ␈↓βif n␈↓α x ␈↓βthen␈↓α y ␈↓βelse a␈↓α x . [␈↓βd␈↓α x * y]]]␈↓.

␈↓ ↓N␈↓Now␈αsuppose␈αwe␈αwould␈αlike␈αto␈αprove␈α␈↓α∀y:[␈↓∧NIL␈↓α␈α*␈αy␈α=␈αy]␈↓.␈α This␈αis␈αquite␈αtrivial;␈αwe␈αneed␈αonly␈αsubstitute
␈↓ ↓N␈↓␈↓∧NIL␈↓ for ␈↓αx␈↓ in (1.2), getting

␈↓ ↓N␈↓␈↓ αN␈↓∧NIL␈↓α * y ␈↓ β.= ␈↓βif n ␈↓∧NIL ␈↓βthen␈↓α y ␈↓βelse a ␈↓∧NIL␈↓α . [␈↓βd ␈↓∧NIL␈↓α * y]

␈↓ ↓N␈↓α␈↓ β.= y␈↓.

␈↓ ↓N␈↓Next␈αconsider␈αproving␈α␈↓α∀x:[x␈α*␈α␈↓∧NIL␈↓α␈α=␈αx]␈↓.␈α This␈αcannot␈αbe␈αdone␈αby␈αsimple␈αsubstitution,␈αbut␈αit␈α
can␈αbe
␈↓ ↓N␈↓done as follows: First substitute ␈↓αλx:[x * ␈↓∧NIL␈↓α = x]␈↓ for ␈↓αP␈↓ in the induction schema

␈↓ ↓N␈↓␈↓α∀u:[islist u ⊃ [␈↓βn␈↓α u ∨ P[␈↓βd␈↓α u] ⊃ P[u]]] ⊃ ∀u:[islist u ⊃ P[u]]␈↓,

␈↓ ↓N␈↓getting

␈↓ ↓N␈↓␈↓α∀u:[islist u ⊃ [␈↓βn␈↓α u ∨ λx:[x * ␈↓∧NIL␈↓α = x][␈↓βd␈↓α u] ⊃ λx:[x * ␈↓∧NIL␈↓α = x][u]]] ⊃ ∀u:[islist u ⊃ λx:[x * ␈↓∧NIL␈↓α = x][u]]␈↓.

␈↓ ↓N␈↓Carrying out the indicated lambda conversions makes this

␈↓ ↓N␈↓␈↓α∀u:[islist u ⊃ [␈↓βn␈↓α u ∨ ␈↓βd␈↓α u * ␈↓∧NIL␈↓α = ␈↓βd␈↓α u] ⊃ u * ␈↓∧NIL␈↓α = u] ⊃ ∀u:[islist u ⊃ u * ␈↓∧NIL␈↓α = u]␈↓.